\begin{tabbing}
$\forall$\=${\it es}$:ES, $C$, $T$:Type, $S$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), $R$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$),\+
\\[0ex]${\it code}$:($j$,$i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $S$($j$,$i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$),
\\[0ex]${\it decode}$:($i$:$C$$\rightarrow$$e$:\{$x$:E$\mid$ $R$($i$,$x$)\} $\rightarrow$state@loc($e$)$\rightarrow$$T$).
\-\\[0ex]for\= clients $C$ sends FIFO\+
\\[0ex]from j to i via ($S$[j,i],${\it code}$)
\\[0ex]receives at i via ($R$[i],${\it decode}$)
\-\\[0ex]$\in$ $\mathbb{P}$
\end{tabbing}